Inference at * 
Iof proof for Lemma adjacent-singleton:


  T:Type, x, y, u:T. adjacent(T;[u];x;y)  False 

latex

 by ((((Unfold `adjacent` 0) 
CollapseTHEN (MaAuto))) 
CollapseTHEN (((Reduce (-1)) 

CoCollapseTHEN (((ExRepD) 
CollapseTHEN (Auto)))))) 

latex

C.

Definitions	adjacent(T;L;x;y), (x  l), , [car / cdr], A List, [], type List, #$n, , l[i], x:A. B(x), x:AB(x), a < b, n - m, -n, n+m, ||as||, t  T, x:A. B(x), x:A  B(x), s = t, Type, {i..j}, {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, Void
Lemmas	false wf, int seg wf, length wf1, select wf